T:Type, u:T, v, L1:T List. L1  v  L1  u.v 

latex

Definitions	t  T, x:A. B(x), L1  L2, P  Q, False, A, tl(l), b
Lemmas	false wf, sublist tl, sublist wf